FDL - Step of Proof: less-fast-fib

Step of Proof: less-fast-fib

Inference at * 2 1
Iof proof for Lemma less-fast-fib:

1.

n, a, b:

.
1. {m:

|
1. {

k:

. (a = fib(k))

((k

0)

(b = 0))

((0 < k)

(b = fib(k - 1)))

(m = fib(n+k))}

n:

. {m:

| m = fib(n)}

by UseWitness

n.f(n,1,0)

1:

1:

(

n.f(n,1,0))

(

n:

. {m:

| m = fib(n)} )

.

Definitions x.A(x), f(a), #$n